; EXPECT: sat
(set-logic QF_ALL)
(set-info :status sat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
(define-fun smt_set_emp () mySet (as set.empty mySet))
(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
(define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2))
(declare-fun z3v58 () Int)
(declare-fun z3v59 () Int)
(assert (distinct z3v58 z3v59))
(declare-fun z3f60 (Int) Bool)
(declare-fun z3v61 () Int)
(declare-fun z3f62 (Int) Int)
(declare-fun z3v63 () Int)
(declare-fun z3v64 () Int)
(declare-fun z3v67 () Int)
(declare-fun z3f68 (Int) Int)
(declare-fun z3f69 (Int) mySet)
(declare-fun z3f70 (Int) mySet)
(declare-fun z3f71 (Int) Bool)
(declare-fun z3v73 () Int)
(declare-fun z3v76 () Int)
(declare-fun z3v79 () Int)
(declare-fun z3v82 () Int)
(declare-fun z3v84 () Int)
(declare-fun z3v85 () Int)
(declare-fun z3v86 () Int)
(declare-fun z3v89 () Int)
(declare-fun z3v90 () Int)
(declare-fun z3v91 () Int)
(declare-fun z3f92 (Int Int) Int)
(declare-fun z3v93 () Int)
(declare-fun z3v94 () Int)
(declare-fun z3f96 () Int)
(declare-fun z3v97 () Int)
(declare-fun z3v98 () Int)
(declare-fun z3v99 () Int)
(declare-fun z3v100 () Int)
(declare-fun z3v101 () Int)
(declare-fun z3v102 () Int)
(declare-fun z3v104 () Int)
(declare-fun z3v107 () Int)
(declare-fun z3v110 () Int)
(declare-fun z3v113 () Int)
(declare-fun z3v116 () Int)
(declare-fun z3v117 () Int)
(declare-fun z3v118 () Int)
(declare-fun z3v119 () Int)
(declare-fun z3v120 () Int)
(declare-fun z3v121 () Int)
(declare-fun z3v122 () Int)
(declare-fun z3v123 () Int)
(declare-fun z3v124 () Int)
(declare-fun z3v125 () Int)
(declare-fun z3v127 () Int)
(declare-fun z3v130 () Int)
(declare-fun z3v133 () Int)
(declare-fun z3v134 () Int)
(declare-fun z3v135 () Int)
(declare-fun z3v136 () Int)
(declare-fun z3v137 () Int)
(declare-fun z3v140 () Int)
(declare-fun z3v141 () Int)
(declare-fun z3v142 () Int)
(declare-fun z3v143 () Int)
(declare-fun z3v144 () Int)
(declare-fun z3v145 () Int)
(declare-fun z3v147 () Int)
(declare-fun z3v150 () Int)
(declare-fun z3v151 () Int)
(declare-fun z3v152 () Int)
(assert (= (z3f69 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v151))))
(assert (= (z3f70 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v151))))
(assert (= (z3f68 z3v152) (+ 1 (z3f68 z3v151))))
(assert (= (z3f71 z3v152) false))
(assert (and (>= (z3f68 z3v140) 0) (>= (z3f68 z3v141) 0) (>= (z3f68 z3v151) 0) (>= (z3f68 z3v142) 0) (= (z3f69 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v141))) (= (z3f68 z3v142) (+ 1 (z3f68 z3v141))) (= (z3f71 z3v142) false) (= z3v142 (z3f92 z3v143 z3v141)) (>= (z3f68 z3v142) 0) (= z3v142 z3v144) (>= (z3f68 z3v142) 0) (>= (z3f68 z3v144) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64)))
(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v141))))
(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140))))
(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v141) (z3f69 z3v140))))
(assert (smt_set_sub (z3f69 z3v151) (z3f69 z3v140)))
(assert (= (z3f69 z3v151) (z3f69 z3v140)))
(assert (<= z3v151 z3v140))
(assert (>= z3v151 z3v140))
(assert (<= (z3f68 z3v151) (z3f68 z3v140)))
(assert (>= (z3f68 z3v151) (z3f68 z3v141)))
(assert (>= (z3f68 z3v151) (z3f68 z3v140)))
(assert (= (z3f68 z3v151) (z3f68 z3v140)))
(assert (= z3v151 z3v140))
(assert (>= (z3f68 z3v151) 0))
(assert (not (= (z3f69 z3v152) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140)))))
(check-sat)
